Software analysis is a common concern among developers. Various techniques can be used to perform software analysis: testing, static analysis, and model checking. Due to complexity of modern software, the above techniques often rely on reduction techniques such as applying analysis to selected parts of the program, called module under analysis. Instead of analyzing the software in its entirety all at once, modular analysis analyzes only one or more modules of the software at a time. To analyze a module in isolation, one needs to model the module's environment, consisting of components with which the module interacts. Once the environment model is generated, it can be combined with the code of the module under analysis, and testing or model checking techniques can be applied to the whole system to check module properties stated as assertions or using a specification language of the underlying analysis technique.
Environment generation is a challenging problem, at least in part because the environment may influence multiple aspects of the behavior of the module being analyzed. Environment may influence the module's control (e.g., by invoking the module's methods) and data (e.g., by passing data to the module). Environment model should be general enough to cover interesting module behaviors and uncover errors, yet restrictive enough to enable tractable analysis, without being overly restrictive, which may cause the analysis to miss important behaviors and mask errors. To evaluate the quality of environment, various metrics can be used. One popular metric is branch coverage. A high quality environment will enable modular software analysis to uncover errors or, in the case of no errors, will produce high branch coverage over the module code.